Inference at * 1 
Iof proof for Lemma decidable assert:



1. b : 
  (b)  ((b)) 

latex

 by BoolInd 1 

latex

 1: 

 1: (no hyps)
 1:   (tt)  ((tt))
 2: 

 2: (no hyps)
 2:   (ff)  ((ff))
 .

Definitions

t  T, Unit, , ff, tt,